|
In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating (or strongly normalizing) abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent.〔Franz Baader, Tobias Nipkow, (1998) ''Term Rewriting and All That'', Cambridge University Press ISBN 0-521-77920-0〕 Equivalently, for every binary relation with no decreasing infinite chains and satisfying a weak version of the diamond property, there is a unique minimal element in every connected component of the relation considered as a graph. Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet in 1980.〔Gérard Huet, "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems", ''Journal of the ACM'' (JACM), October 1980, Volume 27, Issue 4, pp. 797 - 821.〕 Newman's original proof was considerably more complicated.〔Harrison, p. 260, Paterson(1990), p. 354.〕 ==Diamond lemma== In general, Newman's lemma can be seen as a combinatorial result about binary relations → on a set ''A'' (written backwards, so that ''a'' → ''b'' means that ''b'' is below ''a'') with the following two properties: * → is a well-founded relation: every non-empty subset ''X'' of ''A'' has a minimal element (an element ''a'' of ''X'' such that ''a'' → ''b'' for no ''b'' in ''X''). Equivalently, there is no infinite chain . In the terminology of rewriting systems, → is terminating. * Every covering is bounded below. That is, if an element ''a'' in ''A'' covers elements ''b'' and ''c'' in ''A'' in the sense that and , then there is an element ''d'' in ''A'' such that and , where → * denotes the reflexive transitive closure of →. In the terminology of rewriting systems, → is locally confluent. If the above two conditions hold, then the lemma states that → is confluent: whenever and , there is an element ''d'' such that and . In view of the termination of →, this implies that every connected component of → as a graph contains a unique minimal element ''a'', moreover for every element ''b'' of the component.〔Paul M. Cohn, (1980) ''Universal Algebra'', D. Reidel Publishing, ISBN 90-277-1254-9 (''See pp. 25-26'')〕 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Newman's lemma」の詳細全文を読む スポンサード リンク
|